YES(O(1),O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict Trs: { d(x) -> e(u(x)) , d(u(x)) -> c(x) , c(u(x)) -> b(x) , b(u(x)) -> a(e(x)) , v(e(x)) -> x } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'Small Polynomial Path Order (PS,1-bounded)' to orient following rules strictly. Trs: { d(x) -> e(u(x)) , d(u(x)) -> c(x) , c(u(x)) -> b(x) , b(u(x)) -> a(e(x)) , v(e(x)) -> x } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(d) = {}, safe(e) = {1}, safe(u) = {1}, safe(c) = {}, safe(b) = {1}, safe(v) = {}, safe(a) = {1} and precedence d ~ c, d ~ b, d ~ v, c ~ b, c ~ v, b ~ v . Following symbols are considered recursive: {d, c, b} The recursion depth is 1. For your convenience, here are the satisfied ordering constraints: d(x;) > e(; u(; x)) d(u(; x);) > c(x;) c(u(; x);) > b(; x) b(; u(; x)) > a(; e(; x)) v(e(; x);) > x We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { d(x) -> e(u(x)) , d(u(x)) -> c(x) , c(u(x)) -> b(x) , b(u(x)) -> a(e(x)) , v(e(x)) -> x } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^1))